(module types mzscheme
  (require (planet "datatype.ss" ("dherman" "struct.plt" 2 3))
           (lib "plt-match.ss")
           (planet "inspector.ss" ("dherman" "inspector.plt" 1 0)))
  
  (with-public-inspector
   ;; Datatype enumerating the various type constructors
   (define-datatype tycons
     ;; Constants
     (tycon-top ())
     (tycon-bot ())
     
     (tycon-int ())
     (tycon-bool ())
     (tycon-num ())
     
     ;; Instead of representing stack types, we represent type vectors as a list
     ;; ending in a type variable.  For instance, the type 
     ;;    "'A int -> 'A int int"
     ;; would be written as 
     ;;  (cons int 'a) -> (cons int (cons int 'a))
     ;; This has the advantage of allowing type inference to handle type 
     ;; vectors without any special code.
     (tycon-cons ())
     (tycon-null ())
     
     (tycon-tuple ())
     (tycon-list ())
     
     (tycon-pure-arrow   ())
     (tycon-impure-arrow ()))
   
   (define-datatype type
     ;; Type Variable
     (ty-var (identifier))
     
     ;; Application of a type constructor
     (ty-app (tycon args))))
  
  (provide-datatype tycons)
  (provide-datatype type)
  
  (define (valid-arity tycon arity)
    (match tycon
      ((struct tycon-top ())  (= arity 0))
      ((struct tycon-bot ())  (= arity 0))
      ((struct tycon-int ())  (= arity 0))
      ((struct tycon-bool ()) (= arity 0))
      ((struct tycon-num ())  (= arity 0))
      
      ((struct tycon-tuple ()) (>= arity 0))
      ((struct tycon-list ())  (= arity 1))
      
      ((struct tycon-cons ()) (= arity 2))
      ((struct tycon-null ()) (= arity 0))
      
      ((struct tycon-pure-arrow ())   (= arity 2))
      ((struct tycon-impure-arrow ()) (= arity 2))))
  
  (define (symbol-to-tycon symbol)
    (match symbol
      ('top   (make-tycon-top))
      ('bot   (make-tycon-bot))
      ('int   (make-tycon-int))
      ('bool  (make-tycon-bool))
      ('num   (make-tycon-num))
      ('tuple (make-tycon-tuple))
      ('list  (make-tycon-list))
      ('cons  (make-tycon-cons))
      ('null  (make-tycon-null))
      ('->    (make-tycon-pure-arrow))
      ('~>    (make-tycon-impure-arrow))
      (other  #f)))
  
  ;; Generate a new type symbol starting with 'Stack that is gauranteed to be 
  ;; fresh
  (define (fresh-tystackvar)
    (make-ty-var (gensym 'Stack)))
  (define (fresh-tyvar)
    (make-ty-var (gensym 'ty)))
  
  ;; return the arguments to an arrow, or nil if it isn't an arrow
  (define (get-arrow-args arrow)
    (match arrow
      ((struct ty-app (tycon args))
       (and (or (tycon-pure-arrow? tycon) (tycon-impure-arrow? tycon)) args))
      (_ #f)))
  
  ;; Instantiate a type by replacing the type variables used for documentation
  ;; with fresh type variables for this specific instance of the operator
  (define (instantiate ty)
    (let ((env (make-hash-table)))
      (let instantiate ((ty ty))
        (match ty
          ((struct ty-var (id)) 
           (hash-table-get env id
             (lambda () 
               (let ((new-id (if (char-upper-case? (string-ref 
                                                    (symbol->string id) 0))
                                 (fresh-tystackvar)
                                 (fresh-tyvar))))
                 (hash-table-put! env id new-id)
                 new-id))))
          ((struct ty-app (tycon args))
           (make-ty-app tycon (map instantiate args)))))))
  
  (provide valid-arity symbol-to-tycon fresh-tyvar fresh-tystackvar get-arrow-args instantiate)
  )
  